p:FinProbSpace, n:, X, Y:RandomVariable(p;n), a, b:.
E(n;a*X + b*Y) = ((a * E(n;X)) + (b * E(n;Y)))   

latex

Definitions

x:A. B(x), FinProbSpace, , RandomVariable(p;n), E(n;F), X + Y, q*X, t  T, Y, if b then t else f fi , (i = j), tt, P & Q, x. t(x), P  Q, A  B, A, False, , P  Q, P  Q, T, True, , i  j , ff, {i..j}, x(s), i  j < k, , Unit, S  T,

Lemmas

nat wf, finite-prob-space wf, qadd wf, qmul wf, null-seq wf, int seg wf, length wf1, rationals wf, qsum wf, select wf, int inc rationals, l all wf2, qle wf, l member wf, eq int wf, bool wf, assert wf, length wf nat, bnot wf, not wf, weighted-sum wf2, squash wf, true wf, p-outcome wf, expectation wf, random-variable wf, le wf, rv-shift-linear, rv-shift wf, rv-add wf, rv-scale wf, ws-linear, nat properties, ge wf, iff transitivity, eqtt to assert, assert of eq int, eqff to assert, assert of bnot, not functionality wrt iff